perm filename CHANG.EQ[1,JRA] blob sn#005850 filedate 1972-07-14 generic text, type T, neo UTF8
00100	E(T(B B) D);
00200	E(T(C C) G);
00300	E(T(A G) D);
00400	D(X1 B) → ¬D(X1 C);
00500	∀(X1 X2)∃(X3)(D(X1 X2) →E(T(X1 X3) X2));
00600	D(X1 T(X1 X2));
00700	(P(X1) ∧  D(X1 T(X2 X2)))→D(X1 X2);
00800	E(T(X1 T(X2 X3)) T(T(X1 X2) X3));
00900	E(T(X1 X2) T(X2 X1));
01000	(D(X1 X2) ∧ D(X2 X3)) →D(X1 X3);;
01100	;
01200	¬P(A);;